w-machine-independent(w;i;k;x)
== let Choose,Trans,Send = w-machine(w;i) in 
== s1, s2:(x:Idvartype(i;x)).
== (z:Id. ((z = x))  (s1(z) = s2(z)))
==  ((v:w-kindtype(w.TA(i);w.M;i)(k).
==  (((z:Id. ((z = x))  (Trans(k,v,s1,z) = Trans(k,v,s2,z)))
==  ((& Send(k,v,x.s1(x,0)) = Send(k,v,x.s2(x,0)))
==  & ((islocal(k))  (n:. Choose(act(k),n,x.s1(x,0)) = Choose(act(k),n,x.s2(x,0))))) 

latex

---

clarification:

w-machine-independent(w;i;k;x)
== let Choose,Trans,Send = w-machine(w;i) in 
== s1:(x:Idw-vartype(w; i; x)), s2:(x:Idw-vartype(w; i; x)).
== (z:Id. ((z = x  Id))  (s1(z) = s2(z)  w-vartype(w; i; z)))
==  ((v:w-kindtype(w.TA(i);w.M;i)(k).
==  (((z:Id. ((z = x  Id))  (Trans(k,v,s1,z) = Trans(k,v,s2,z)  w-vartype(w; i; z)))
==  ((& Send(k,v,x.s1(x,0)) = Send(k,v,x.s2(x,0))  (w-Msg(w) List))
==  & ((islocal(k))
==  & ( (n:.
==  & ( Choose(act(k),n,x.s1(x,0))
==  & ( =
==  & ( Choose(act(k),n,x.s2(x,0))
==  & (  ((w-kindtype(w.TA(i);w.M;i)(k)) + Unit)))) 

latex

Definitions	let x,y,z = a in t(x;y;z), w-machine(w;i), P & Q, A, Id, x:AB(x), , vartype(i;x), type List, Msg, P  Q, b, islocal(k), x:A. B(x), , s = t, left + right, w-kindtype(TA;M;i), w.TA, w.M, Unit, act(k), x.A(x), f(a), #$n
FDL editor aliases	w-machine-independent